Nuprl Lemma : map_append_sq
11,40
postcript
pdf
f
,
as'
:top,
A
:Type,
as
:(
A
List).
sqequal(map(
f
; append(
as
;
as'
)); append(map(
f
;
as
); map(
f
;
as'
)))
latex
Definitions
t
T
,
Y
,
append(
as
;
bs
)
,
map(
f
;
as
)
,
x
:
A
.
B
(
x
)
Lemmas
top
wf
origin
f,as':top, A:Type, as:(A List).
f,as':top, A:Type, as:(A List).
Tx:A. B(x)